Affiner les résultats

Using linear algebra in decomposition of Farkas interpolants

Blicha, Martin ; Hyvärinen, Antti E. J. ; Kofroň, Jan ; Sharygina, Natasha

In: International journal on software tools for technology transfer, 2021, p. 15

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by ...